#!/bin/csh -f
make OPTFLAGS='-O5 $(ABKSYMBOLS)' RHKEY="-R" $1 $2 $3 $4 $5

